l:IdLnk, p:(IdLnk List).
lpath([l / p])
 (lpath(p)
 & (((||p|| = 0))
 & ( (destination(l) = source(hd(p))  Id & ((hd(p) = lnk-inv(l)  IdLnk))))) 

latex

Definitions	x:A. B(x), P  Q, P & Q, P  Q, P  Q, t  T, , lpath(p), T, True, hd(l), l[i], nth_tl(n;as), Y, if b then t else f fi , i z j, b, i <z j, tt, ff, A, ||as||, False, SQType(T), {T}, tl(l), {i..j}, i  j < k, A  B, Dec(P), P  Q
Lemmas	not wf, length wf1, IdLnk wf, lpath wf, Id wf, ldst wf, lsrc wf, hd wf, non neg length, lnk-inv wf, length cons, squash wf, true wf, select cons tl, int seg wf, decidable int equal, select wf, le wf